package org.checkerframework.framework.util.typeinference8.types;

import com.sun.source.tree.ExpressionTree;
import java.util.EnumMap;
import java.util.LinkedHashSet;
import java.util.Objects;
import java.util.Set;
import javax.lang.model.element.AnnotationMirror;
import org.checkerframework.framework.util.typeinference8.constraint.Constraint.Kind;
import org.checkerframework.framework.util.typeinference8.constraint.ConstraintSet;
import org.checkerframework.framework.util.typeinference8.constraint.QualifierTyping;
import org.checkerframework.framework.util.typeinference8.types.VariableBounds.BoundKind;
import org.checkerframework.framework.util.typeinference8.util.Java8InferenceContext;

/**
 * A {@code QualifierVar} is a variable for a polymorphic qualifier that needs to be viewpoint
 * adapted at a call site.
 */
public class QualifierVar extends AbstractQualifier {

  /** Identification number. Used only to make debugging easier. */
  protected final int id;

  /**
   * The expression for which this variable is being solved. Used to differentiate qualifier
   * variables for two different invocations of the same method or constructor.
   */
  protected final ExpressionTree invocation;

  /** The polymorphic qualifier associated with this var. */
  protected final AnnotationMirror polyQualifier;

  /** A mapping from a {@link BoundKind} to a set of abstract qualifiers. */
  public final EnumMap<BoundKind, Set<AbstractQualifier>> qualifierBounds =
      new EnumMap<>(BoundKind.class);

  /** The instantiation of this variable. This is set during inference. */
  protected AnnotationMirror instantiation;

  /**
   * Creates a {@link QualifierVar}.
   *
   * @param invocation the expression for which this variable is being solved
   * @param polyQualifier polymorphic qualifier associated with this var
   * @param context the context
   */
  public QualifierVar(
      ExpressionTree invocation, AnnotationMirror polyQualifier, Java8InferenceContext context) {
    super(polyQualifier, context);
    this.id = context.getNextVariableId();
    this.invocation = invocation;
    this.polyQualifier = polyQualifier;
    qualifierBounds.put(BoundKind.EQUAL, new LinkedHashSet<>());
    qualifierBounds.put(BoundKind.UPPER, new LinkedHashSet<>());
    qualifierBounds.put(BoundKind.LOWER, new LinkedHashSet<>());
  }

  @Override
  public boolean equals(Object o) {
    if (this == o) {
      return true;
    }
    if (o == null || getClass() != o.getClass()) {
      return false;
    }
    QualifierVar that = (QualifierVar) o;
    return id == that.id
        && Objects.equals(invocation, that.invocation)
        && Objects.equals(polyQualifier, that.polyQualifier);
  }

  @Override
  public int hashCode() {
    return Objects.hash(id, invocation, polyQualifier);
  }

  @Override
  public String toString() {
    return "@QV" + id;
  }

  /**
   * Add a bound for this qualifier variable.
   *
   * @param kind a bound kind
   * @param otherQual the bound to add
   * @return a set of constraints generated from adding this bound
   */
  @SuppressWarnings("interning:not.interned") // Checking for exact object.
  public ConstraintSet addBound(BoundKind kind, AbstractQualifier otherQual) {
    if (otherQual == this) {
      return ConstraintSet.TRUE;
    }
    if (kind == BoundKind.EQUAL && otherQual instanceof Qualifier) {
      instantiation = ((Qualifier) otherQual).getAnnotation();
    }
    if (qualifierBounds.get(kind).add(otherQual)) {
      return addConstraintsFromComplementaryBounds(kind, otherQual);
    }
    return ConstraintSet.TRUE;
  }

  /**
   * Returns the constraints generated by adding the given bound.
   *
   * @param kind bound kind
   * @param s other abstract qualifier
   * @return the constraints
   */
  @SuppressWarnings("interning:not.interned") // Checking for exact object.
  private ConstraintSet addConstraintsFromComplementaryBounds(BoundKind kind, AbstractQualifier s) {
    ConstraintSet constraints = new ConstraintSet();
    switch (kind) {
      case EQUAL:
        for (AbstractQualifier t : qualifierBounds.get(BoundKind.EQUAL)) {
          if (s != t) {
            constraints.add(new QualifierTyping(s, t, Kind.TYPE_EQUALITY));
          }
        }
        break;
      case LOWER:
        for (AbstractQualifier t : qualifierBounds.get(BoundKind.EQUAL)) {
          if (s != t) {
            constraints.add(new QualifierTyping(s, t, Kind.SUBTYPE));
          }
        }
        break;
      case UPPER:
        for (AbstractQualifier t : qualifierBounds.get(BoundKind.EQUAL)) {
          if (s != t) {
            constraints.add(new QualifierTyping(t, s, Kind.SUBTYPE));
          }
        }
        break;
    }

    if (kind == BoundKind.EQUAL || kind == BoundKind.UPPER) {
      for (AbstractQualifier t : qualifierBounds.get(BoundKind.LOWER)) {
        if (s != t) {
          constraints.add(new QualifierTyping(t, s, Kind.SUBTYPE));
        }
      }
    }

    if (kind == BoundKind.EQUAL || kind == BoundKind.LOWER) {
      for (AbstractQualifier t : qualifierBounds.get(BoundKind.UPPER)) {
        if (s != t) {
          constraints.add(new QualifierTyping(s, t, Kind.SUBTYPE));
        }
      }
    }
    return constraints;
  }

  @Override
  AnnotationMirror getInstantiation() {
    if (instantiation == null) {
      AnnotationMirror lub = null;
      for (AbstractQualifier lower : qualifierBounds.get(BoundKind.LOWER)) {
        if (lower instanceof Qualifier) {
          if (lub != null) {
            lub =
                context
                    .typeFactory
                    .getQualifierHierarchy()
                    .leastUpperBoundQualifiersOnly(lub, ((Qualifier) lower).getAnnotation());
          } else {
            lub = ((Qualifier) lower).getAnnotation();
          }
        }
      }
      if (lub != null) {
        instantiation = lub;
        return instantiation;
      }
      AnnotationMirror glb = null;
      for (AbstractQualifier upper : qualifierBounds.get(BoundKind.UPPER)) {
        if (upper instanceof Qualifier) {
          if (glb != null) {
            glb =
                context
                    .typeFactory
                    .getQualifierHierarchy()
                    .greatestLowerBoundQualifiersOnly(glb, ((Qualifier) upper).getAnnotation());
          } else {
            glb = ((Qualifier) upper).getAnnotation();
          }
        }
      }
      return glb;
    }
    return instantiation;
  }
}
